p:. ((p))  ((p)) 

latex

ProofTree

Definitions	t  T, P  Q, P  Q, x:A. B(x), ff, if b then t else f fi , tt, A, b, b, P  Q, , True, P  Q, False, Unit, ,
Lemmas	bool wf, true wf, false wf